InforLorV4, Main, Exploration, bibRecord, 004C19

Noetherianity and Combination Problems

Identifieur interne : 004C19 ( Main/Exploration ); précédent : 004C18; suivant : 004C20

Noetherianity and Combination Problems

Auteurs : Silvio Ghilardi [Italie] ; Enrica Nicolini [France] ; Silvio Ranise [France] ; Daniele Zucchelli [Italie, France]

Source :

Lecture Notes in Computer Science [ 0302-9743 ]

RBID : ISTEX:C991BB9C30368FB95A0F1CA39AC57EB47A6A0022

Abstract

Abstract: In abstract algebra, a structure is said to be Noetherian if it does not admit infinite strictly ascending chains of congruences. In this paper, we adapt this notion to first-order logic by defining the class of Noetherian theories. Examples of theories in this class are Linear Arithmetics without ordering and the empty theory containing only a unary function symbol. Interestingly, it is possible to design a non-disjoint combination method for extensions of Noetherian theories. We investigate sufficient conditions for adding a temporal dimension to such theories in such a way that the decidability of the satisfiability problem for the quantifier-free fragment of the resulting temporal logic is guaranteed. This problem is firstly investigated for the case of Linear time Temporal Logic and then generalized to arbitrary modal/temporal logics whose propositional relativized satisfiability problem is decidable.

Url:

DOI: 10.1007/978-3-540-74621-8_14

Affiliations:

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Noetherianity and Combination Problems</title>
<author><name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name>
</author>
<author><name sortKey="Nicolini, Enrica" sort="Nicolini, Enrica" uniqKey="Nicolini E" first="Enrica" last="Nicolini">Enrica Nicolini</name>
</author>
<author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name>
</author>
<author><name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:C991BB9C30368FB95A0F1CA39AC57EB47A6A0022</idno>
<date when="2007" year="2007">2007</date>
<idno type="doi">10.1007/978-3-540-74621-8_14</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-TM17W6GL-2/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">002F80</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002F80</idno>
<idno type="wicri:Area/Istex/Curation">002F41</idno>
<idno type="wicri:Area/Istex/Checkpoint">001004</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001004</idno>
<idno type="wicri:doubleKey">0302-9743:2007:Ghilardi S:noetherianity:and:combination</idno>
<idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:inria-00576594</idno>
<idno type="url">https://hal.inria.fr/inria-00576594</idno>
<idno type="wicri:Area/Hal/Corpus">003592</idno>
<idno type="wicri:Area/Hal/Curation">003592</idno>
<idno type="wicri:Area/Hal/Checkpoint">003869</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">003869</idno>
<idno type="wicri:Area/Main/Merge">004D53</idno>
<idno type="wicri:Area/Main/Curation">004C19</idno>
<idno type="wicri:Area/Main/Exploration">004C19</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Noetherianity and Combination Problems</title>
<author><name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name>
<affiliation wicri:level="1"><country xml:lang="fr">Italie</country>
<wicri:regionArea>Dipartimento di Informatica, Università degli Studi di Milano</wicri:regionArea>
<wicri:noRegion>Università degli Studi di Milano</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Nicolini, Enrica" sort="Nicolini, Enrica" uniqKey="Nicolini E" first="Enrica" last="Nicolini">Enrica Nicolini</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA & INRIA-Lorraine, Nancy</wicri:regionArea>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
</affiliation>
</author>
<author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA & INRIA-Lorraine, Nancy</wicri:regionArea>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
</affiliation>
</author>
<author><name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name>
<affiliation wicri:level="1"><country xml:lang="fr">Italie</country>
<wicri:regionArea>Dipartimento di Informatica, Università degli Studi di Milano</wicri:regionArea>
<wicri:noRegion>Università degli Studi di Milano</wicri:noRegion>
</affiliation>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA & INRIA-Lorraine, Nancy</wicri:regionArea>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<idno type="ISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: In abstract algebra, a structure is said to be Noetherian if it does not admit infinite strictly ascending chains of congruences. In this paper, we adapt this notion to first-order logic by defining the class of Noetherian theories. Examples of theories in this class are Linear Arithmetics without ordering and the empty theory containing only a unary function symbol. Interestingly, it is possible to design a non-disjoint combination method for extensions of Noetherian theories. We investigate sufficient conditions for adding a temporal dimension to such theories in such a way that the decidability of the satisfiability problem for the quantifier-free fragment of the resulting temporal logic is guaranteed. This problem is firstly investigated for the case of Linear time Temporal Logic and then generalized to arbitrary modal/temporal logics whose propositional relativized satisfiability problem is decidable.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
<li>Italie</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
</region>
<settlement><li>Nancy</li>
</settlement>
</list>
<tree><country name="Italie"><noRegion><name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name>
</noRegion>
<name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name>
</country>
<country name="France"><region name="Grand Est"><name sortKey="Nicolini, Enrica" sort="Nicolini, Enrica" uniqKey="Nicolini E" first="Enrica" last="Nicolini">Enrica Nicolini</name>
</region>
<name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name>
<name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004C19 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 004C19 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     ISTEX:C991BB9C30368FB95A0F1CA39AC57EB47A6A0022
   |texte=   Noetherianity and Combination Problems
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

Serveur d'exploration sur la recherche en informatique en Lorraine

Noetherianity and Combination Problems

Noetherianity and Combination Problems

Source :

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.